Nuprl Definition : rel_plus
0,22
postcript
pdf
R
^+(
x
,
y
) ==
n
:
.
x
rel_exp(
T
;
R
;
n
)
y
latex
clarification:
rel_plus(
T
;
R
)(
x
,
y
) ==
n
:
.
x
rel_exp(
T
;
R
;
n
)
y
latex
Definitions
rel_exp(
T
;
R
;
n
)
,
x
f
y
,
,
x
:
A
.
B
(
x
)
FDL editor aliases
rel_plus
origin
n:
. x rel_exp(T;R;n) y
n:. x rel_exp(T;R;n) y n:. x rel_exp(T;R;n) y
n:. x rel_exp(T;R;n) y x:A. B(x)